Inference at * 1 1 2 1 
Iof proof for Lemma add functionality wrt le:



1. i2 : 
2. j2 : 
3. i2  j2
4. j1 : 
5. 0 < j1
6. (0  (j1 - 1))  ((0+i2)  ((j1 - 1)+j2))
7. 0  j1
  (0+i2)  (j1+j2) 

latex

 by (RA (D 6)) 

latex

 .

Definitions

t  T, False, A, P  Q, A  B